Nuprl Lemma : s_part_char
13,42
postcript
pdf
T
:Type,
R
:(
T
T
),
a
,
b
:
T
. (
R
\)(
a
,
b
) = (
R
(
a
,
b
) & (
(
R
(
b
,
a
))))
latex
Up
gen
algebra
1
Definitions of Statement
E
\
Definitions
t
T
,
P
&
Q
,
E
\
,
,
x
:
A
.
B
(
x
)
Lemmas
not
wf
origin
T:Type, R:(T
T
), a, b:T. (R\)(a,b) = (R(a,b) & (
(R(b,a)))) 
T:Type, R:(TT), a, b:T. (R\)(a,b) = (R(a,b) & ((R(b,a)))) Tx:A. B(x)